A:Realizer. ((Rplus?(A)))  (R-size(A) = 1) 

latex

Definitions	True, if b then t else f fi , tt, ff, x. t(x), t  T, R-size(R), Rplus?(x1), b, P  Q, x:A. B(x), False, x(s), Unit, A, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, , Rnone(),
Lemmas	es realizer wf, true wf, false wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf